(proof lisp)

(DECL (U V W) |GROUND| VARIABLE LIST)

(DECL (X Y Z) |GROUND| VARIABLE SEXP)

(decl (a b c) |ground| variable)

(decl phi |ground→truthval| variable)

(DECL (NNIL) |GROUND| CONSTANT LIST)

(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)

(DECL (CAR CDR) |GROUND→GROUND| CONSTANT)

(DECL (NULL) |GROUND→TRUTHVAL| CONSTANT)

(DECL (list) |GROUND→TRUTHVAL| CONSTANT)

(DECL (sexp) |GROUND→TRUTHVAL| CONSTANT)

(axiom |∀u.list(u)|)

(axiom |∀u.sexp(u)|)

(axiom |∀x.sexp(x)|)

(AXIOM |∀X U.list(CONS(X,U))|)

(AXIOM |∀U.NULL(U)≡U=NNIL|)

(axiom |∀x u.¬null(cons(x,u))|)

(axiom |∀x u.car(cons(x,u)) = x|)

(axiom |∀x u.cdr(cons(x,u)) = u|)

(decl copy |ground→ground| constant)

(axiom |∀u.copy(u) = if null(u) then nnil else cons(car(u),copy(cdr(u)))|)

(axiom |∀phi.phi(nnil) ∧ (∀x u.phi(u) ⊃ phi(cons(x,u))) ⊃ ∀u.phi(u)|)

(∀e phi |λv.(copy(v)=v)| 21 14)